*****************************************************
Commutativity of set union

(thorn.defaults)

(define st
  {--> symbol}
  -> (kb-> [[all x [~ [m x e]]]
                [all x [all y [[[sub x y] & [sub y x]] <=> [=s x y]]]]
                [all x [all y [[sub x y] <=> [all z [[m z x] => [m z y]]]]]]
                [all x [all y [[pow x y] <=> [all z [[m z x] <=> [sub z y]]]]]]
                [all x [all y [[com x y] <=> [all z [[m z x] <=> [~ [m z y]]]]]]]
                [all x [all y [all z [[prod x y z] <=> [all w [[m w x] <=> [[pair w] & [[m [fst w] y] & [m [snd w] z]]]]]]]]] 
                [all x [all y [all z [[int x y z] <=> [all w [[m w x] <=> [[m w y] & [m w z]]]]]]]]
                [all x [all y [all z [[un x y z] <=> [all w [[m w x] <=> [[m w y] v [m w z]]]]]]]]]))
                
(st)                      
     
(<-kb  [all x [all y [all z [[un x y z] <=> [un x z y]]]]])

run time: 0.3125 secs
440722 inferences, equality = false
depth = 20, complexity = -1, timeout = 60 secs
true

****************************************************
Step 1

? (all x (all y (all z ((un x y z) <=> (un x z y)))))


> revsk
=============================
Step 2

? (((~ (un c59127 c59126 c59125)) v (un c59127 c59125 c59126)) & ((~ (un c59127 c59125 c59126)) v (un c59127 c59126 c59125)))


> &r
|=============================
|Step 3
|
|? ((~ (un c59127 c59126 c59125)) v (un c59127 c59125 c59126))
|
|
|> hypdisj
|=============================
|Step 4
|
|? (un c59127 c59125 c59126)
|
|1. (un c59127 c59126 c59125)
|
|> ((un W X Y) <-- (~ (m (f50305 W X Y Z) X)) (~ (m (f50305 W X Y Z) Y)) (~ (m (f50305 W X Y Z) W)))
|||=============================
|||Step 5
|||
|||? (~ (m (f50305 c59127 c59125 c59126 Var96) c59125))
|||
|||1. (~ (un c59127 c59125 c59126))
|||2. (un c59127 c59126 c59125)
|||
|||> ((~ (m Z Y)) <-- (un W X Y) (~ (m Z W)))
||||=============================
||||Step 6
||||
||||? (un Var100 Var99 c59125)
||||
||||1. (m (f50305 c59127 c59125 c59126 Var96) c59125)
||||2. (~ (un c59127 c59125 c59126))
||||3. (un c59127 c59126 c59125)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (m (f50305 c59127 c59125 c59126 Var96) c59127))
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59125)
|||2. (~ (un c59127 c59125 c59126))
|||3. (un c59127 c59126 c59125)
|||
|||> ((~ (m (f50305 X W Y Z) X)) <-- (~ (un X W Y)) (m (f50305 X W Y Z) W))
||||=============================
||||Step 8
||||
||||? (~ (un c59127 c59125 c59126))
||||
||||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
||||2. (m (f50305 c59127 c59125 c59126 Var96) c59125)
||||3. (~ (un c59127 c59125 c59126))
||||4. (un c59127 c59126 c59125)
||||
||||> hyp
|||=============================
|||Step 9
|||
|||? (m (f50305 c59127 c59125 c59126 Var96) c59125)
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|||2. (m (f50305 c59127 c59125 c59126 Var96) c59125)
|||3. (~ (un c59127 c59125 c59126))
|||4. (un c59127 c59126 c59125)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (m (f50305 c59127 c59125 c59126 Var96) c59126))
||
||1. (~ (un c59127 c59125 c59126))
||2. (un c59127 c59126 c59125)
||
||> ((~ (m Z X)) <-- (un W X Y) (~ (m Z W)))
|||=============================
|||Step 11
|||
|||? (un Var109 c59126 Var108)
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59126)
|||2. (~ (un c59127 c59125 c59126))
|||3. (un c59127 c59126 c59125)
|||
|||> hyp
||=============================
||Step 12
||
||? (~ (m (f50305 c59127 c59125 c59126 Var96) c59127))
||
||1. (m (f50305 c59127 c59125 c59126 Var96) c59126)
||2. (~ (un c59127 c59125 c59126))
||3. (un c59127 c59126 c59125)
||
||> ((~ (m (f50305 X Y W Z) X)) <-- (~ (un X Y W)) (m (f50305 X Y W Z) W))
|||=============================
|||Step 13
|||
|||? (~ (un c59127 c59125 c59126))
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|||2. (m (f50305 c59127 c59125 c59126 Var96) c59126)
|||3. (~ (un c59127 c59125 c59126))
|||4. (un c59127 c59126 c59125)
|||
|||> hyp
||=============================
||Step 14
||
||? (m (f50305 c59127 c59125 c59126 Var96) c59126)
||
||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
||2. (m (f50305 c59127 c59125 c59126 Var96) c59126)
||3. (~ (un c59127 c59125 c59126))
||4. (un c59127 c59126 c59125)
||
||> hyp
|=============================
|Step 15
|
|? (~ (m (f50305 c59127 c59125 c59126 Var96) c59127))
|
|1. (~ (un c59127 c59125 c59126))
|2. (un c59127 c59126 c59125)
|
|> ((~ (m Z X)) <-- (un X Y W) (~ (m Z Y)) (~ (m Z W)))
|||=============================
|||Step 16
|||
|||? (un c59127 Var117 Var118)
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|||2. (~ (un c59127 c59125 c59126))
|||3. (un c59127 c59126 c59125)
|||
|||> hyp
||=============================
||Step 17
||
||? (~ (m (f50305 c59127 c59125 c59126 Var96) c59126))
||
||1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
||2. (~ (un c59127 c59125 c59126))
||3. (un c59127 c59126 c59125)
||
||> ((~ (m (f50305 W X Y Z) Y)) <-- (~ (un W X Y)) (m (f50305 W X Y Z) W))
|||=============================
|||Step 18
|||
|||? (~ (un c59127 c59125 c59126))
|||
|||1. (m (f50305 c59127 c59125 c59126 Var96) c59126)
|||2. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|||3. (~ (un c59127 c59125 c59126))
|||4. (un c59127 c59126 c59125)
|||
|||> hyp
||=============================
||Step 19
||
||? (m (f50305 c59127 c59125 c59126 Var96) c59127)
||
||1. (m (f50305 c59127 c59125 c59126 Var96) c59126)
||2. (m (f50305 c59127 c59125 c59126 Var96) c59127)
||3. (~ (un c59127 c59125 c59126))
||4. (un c59127 c59126 c59125)
||
||> hyp
|=============================
|Step 20
|
|? (~ (m (f50305 c59127 c59125 c59126 Var96) c59125))
|
|1. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|2. (~ (un c59127 c59125 c59126))
|3. (un c59127 c59126 c59125)
|
|> ((~ (m (f50305 W X Y Z) X)) <-- (~ (un W X Y)) (m (f50305 W X Y Z) W))
||=============================
||Step 21
||
||? (~ (un c59127 c59125 c59126))
||
||1. (m (f50305 c59127 c59125 c59126 Var96) c59125)
||2. (m (f50305 c59127 c59125 c59126 Var96) c59127)
||3. (~ (un c59127 c59125 c59126))
||4. (un c59127 c59126 c59125)
||
||> hyp
|=============================
|Step 22
|
|? (m (f50305 c59127 c59125 c59126 Var96) c59127)
|
|1. (m (f50305 c59127 c59125 c59126 Var96) c59125)
|2. (m (f50305 c59127 c59125 c59126 Var96) c59127)
|3. (~ (un c59127 c59125 c59126))
|4. (un c59127 c59126 c59125)
|
|> hyp
=============================
Step 23

? ((~ (un c59127 c59125 c59126)) v (un c59127 c59126 c59125))


> hypdisj
=============================
Step 24

? (un c59127 c59126 c59125)

1. (un c59127 c59125 c59126)

> ((un W X Y) <-- (~ (m (f50305 W X Y Z) X)) (~ (m (f50305 W X Y Z) Y)) (~ (m (f50305 W X Y Z) W)))
||=============================
||Step 25
||
||? (~ (m (f50305 c59127 c59126 c59125 Var134) c59126))
||
||1. (~ (un c59127 c59126 c59125))
||2. (un c59127 c59125 c59126)
||
||> ((~ (m Z Y)) <-- (un W X Y) (~ (m Z W)))
|||=============================
|||Step 26
|||
|||? (un Var138 Var137 c59126)
|||
|||1. (m (f50305 c59127 c59126 c59125 Var134) c59126)
|||2. (~ (un c59127 c59126 c59125))
|||3. (un c59127 c59125 c59126)
|||
|||> hyp
||=============================
||Step 27
||
||? (~ (m (f50305 c59127 c59126 c59125 Var134) c59127))
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59126)
||2. (~ (un c59127 c59126 c59125))
||3. (un c59127 c59125 c59126)
||
||> ((~ (m (f50305 X W Y Z) X)) <-- (~ (un X W Y)) (m (f50305 X W Y Z) W))
|||=============================
|||Step 28
|||
|||? (~ (un c59127 c59126 c59125))
|||
|||1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
|||2. (m (f50305 c59127 c59126 c59125 Var134) c59126)
|||3. (~ (un c59127 c59126 c59125))
|||4. (un c59127 c59125 c59126)
|||
|||> hyp
||=============================
||Step 29
||
||? (m (f50305 c59127 c59126 c59125 Var134) c59126)
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
||2. (m (f50305 c59127 c59126 c59125 Var134) c59126)
||3. (~ (un c59127 c59126 c59125))
||4. (un c59127 c59125 c59126)
||
||> hyp
|=============================
|Step 30
|
|? (~ (m (f50305 c59127 c59126 c59125 Var134) c59125))
|
|1. (~ (un c59127 c59126 c59125))
|2. (un c59127 c59125 c59126)
|
|> ((~ (m Z X)) <-- (un W X Y) (~ (m Z W)))
||=============================
||Step 31
||
||? (un Var147 c59125 Var146)
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59125)
||2. (~ (un c59127 c59126 c59125))
||3. (un c59127 c59125 c59126)
||
||> hyp
|=============================
|Step 32
|
|? (~ (m (f50305 c59127 c59126 c59125 Var134) c59127))
|
|1. (m (f50305 c59127 c59126 c59125 Var134) c59125)
|2. (~ (un c59127 c59126 c59125))
|3. (un c59127 c59125 c59126)
|
|> ((~ (m (f50305 X Y W Z) X)) <-- (~ (un X Y W)) (m (f50305 X Y W Z) W))
||=============================
||Step 33
||
||? (~ (un c59127 c59126 c59125))
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
||2. (m (f50305 c59127 c59126 c59125 Var134) c59125)
||3. (~ (un c59127 c59126 c59125))
||4. (un c59127 c59125 c59126)
||
||> hyp
|=============================
|Step 34
|
|? (m (f50305 c59127 c59126 c59125 Var134) c59125)
|
|1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
|2. (m (f50305 c59127 c59126 c59125 Var134) c59125)
|3. (~ (un c59127 c59126 c59125))
|4. (un c59127 c59125 c59126)
|
|> hyp
=============================
Step 35

? (~ (m (f50305 c59127 c59126 c59125 Var134) c59127))

1. (~ (un c59127 c59126 c59125))
2. (un c59127 c59125 c59126)

> ((~ (m Z X)) <-- (un X Y W) (~ (m Z Y)) (~ (m Z W)))
||=============================
||Step 36
||
||? (un c59127 Var155 Var156)
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
||2. (~ (un c59127 c59126 c59125))
||3. (un c59127 c59125 c59126)
||
||> hyp
|=============================
|Step 37
|
|? (~ (m (f50305 c59127 c59126 c59125 Var134) c59125))
|
|1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
|2. (~ (un c59127 c59126 c59125))
|3. (un c59127 c59125 c59126)
|
|> ((~ (m (f50305 W X Y Z) Y)) <-- (~ (un W X Y)) (m (f50305 W X Y Z) W))
||=============================
||Step 38
||
||? (~ (un c59127 c59126 c59125))
||
||1. (m (f50305 c59127 c59126 c59125 Var134) c59125)
||2. (m (f50305 c59127 c59126 c59125 Var134) c59127)
||3. (~ (un c59127 c59126 c59125))
||4. (un c59127 c59125 c59126)
||
||> hyp
|=============================
|Step 39
|
|? (m (f50305 c59127 c59126 c59125 Var134) c59127)
|
|1. (m (f50305 c59127 c59126 c59125 Var134) c59125)
|2. (m (f50305 c59127 c59126 c59125 Var134) c59127)
|3. (~ (un c59127 c59126 c59125))
|4. (un c59127 c59125 c59126)
|
|> hyp
=============================
Step 40

? (~ (m (f50305 c59127 c59126 c59125 Var134) c59126))

1. (m (f50305 c59127 c59126 c59125 Var134) c59127)
2. (~ (un c59127 c59126 c59125))
3. (un c59127 c59125 c59126)

> ((~ (m (f50305 W X Y Z) X)) <-- (~ (un W X Y)) (m (f50305 W X Y Z) W))
|=============================
|Step 41
|
|? (~ (un c59127 c59126 c59125))
|
|1. (m (f50305 c59127 c59126 c59125 Var134) c59126)
|2. (m (f50305 c59127 c59126 c59125 Var134) c59127)
|3. (~ (un c59127 c59126 c59125))
|4. (un c59127 c59125 c59126)
|
|> hyp
=============================
Step 42

? (m (f50305 c59127 c59126 c59125 Var134) c59127)

1. (m (f50305 c59127 c59126 c59125 Var134) c59126)
2. (m (f50305 c59127 c59126 c59125 Var134) c59127)
3. (~ (un c59127 c59126 c59125))
4. (un c59127 c59125 c59126)

> hyp
